perm filename PASCRP[P,JRA] blob
sn#442101 filedate 1979-05-17 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 lisp programs for generating pascal
C00034 00003 (*pascal programs*)
C00059 ENDMK
C⊗;
;lisp programs for generating pascal
;each function specification gets turned into a complete program so that
;a library of functions can be built. Each function is declared external.
;the surrounding program is just a dummy to satisfy syntax restrictions.
;a type specification is turned into a type declaration and stuffed on the
;property list of the type name(under 'type-dec), to be
;included in the declaration of every
;function that uses the type. (apparently there is no such thing as an
;external type in pascal, so it has to be re-declared everywhere)
; (list 'program '/ (gensym) '/, name '(input /, output) '; '/
;)
(def make_pascal_def ()
(append
(list 'program '/ (gensym) '/, name '/; '/
)
(make-type-decs) ;makes the definitions for all types used
;i.e., termlists, terms, constants, symbols,
; and whatever else is necessary as subtypes
(make-external-decs (get name 'external-procs))
(list 'function '/ name (rest (make-parameter-list
(strip! (get name 'params))
(get name 'inpat)))
': '/ 'boolean '/; '/
)
(make-body-of name);dont forget to include: new(actuals);
(list 'begin '/ ; actuals↑.sl := true;
'end '/.)
))
(def strip! (varlist)
(cond ((null varlist) ())
(t (cons ((lambda (namelist)
(cond ((eq (first namelist) '!)
(implode (rest namelist)))
(t (first varlist))))
(explode (first varlist)))
(strip! (rest varlist))))))
(def make-parameter-list (params inpat) ;declares all formals to be type term, but
(cond ((null params)()) ;leaves an extra ";" on the
(t (append ; front of the list
((lambda (arg)
((lambda (first-dec)
(cond ((eq (first inpat) 0)
(append '(/; var) first-dec))
(t (cons '/; first-dec))))
(list arg ': 'term)))
(first params))
(make-parameter-list (rest params) (rest inpat))))))
;(def is-fun (name) (get name 'function))
;(def make-parameter-list (params inpat) ;deletes the leading ";" and <cr>
; (rest (rest (make-par-list params inpat)))) ;left by make-par-list
;every formal parameter is of type TERM
;(def make-par-list (formal-params inpat)
; (cond ((null formal-params) ())
; (t (append ((lambda (param)
; ((lambda (first-dec)
; (cond ((eq (first inpat) 0)
; (append '(; var) first-dec))
; (t (cons '; first-dec))))
; (list param ': 'TERM )))
; (first formal-params))
; (make-par-list (rest formal-params) (rest inpat))))))
;
;every local used by the spec must be of type TERM
(def make-local-decs (locals) ;takes a 4 element list of vars to be declared as
(append '(var /
;termlists, terms, constants, and
) ;symbols, and returns a list that
(cons '/ (rest ;consists of the pascal to do it
(rest (make-decs (first locals)
'termlist))))
(cons '/ (rest
(rest (make-decs (second locals)
'term))))
(cond ((null (third locals)) ()) (t
(cons '/ (rest
(rest (make-decs (third locals)
'constant))))))
(cond ((null (fourth locals)) ()) (t
(cons '/ (rest
(rest (make-decs (fourth locals)
'symbol))))))))
(def make-decs (vars type) ;makes a list of vars : type, leaves an extra ","
(cond ((null vars) (list ': '/ type'/;'/
)) ;and " " on front
(t (append (list '/, '/ (first vars))
(make-decs (rest vars) type)))))
(def make-type-decs ()
'(type /
/ alltyps / = / /( integertyp /, realtyp /, booleantyp /,
chartyp /, symboltyp /) /; /
/
/ termtyps / =/ /( variable /, / constanttyp /, / funapp /)/;/
/
/ term / =/ ↑t1 /;/
/
/ termlist/ =/ ↑tl1/;/
/
/ constant/ =/ ↑c1/;/
/
/ symbol/ =/ ↑sym1/;/
/
/ t1/ =/ record/
/ / case / ttyp:termtyps / of/
/ / / variable:/ /(vr:/ integer/)/;/
/ / / constanttyp:/ /(cnst:/ constant/)/;/
/ / / funapp:/ /(fname:/ symbol/;/
/ / / / / args:/ termlist/)/
/ / end/;/
/
/ tl1/ =/ record/
/ / notempty:/ boolean/;/
/ / first:/ term/;/
/ / rest:/ termlist/
/ / end/;/
/
/ c1/ =/ record/
/ / case/ ctyp:alltyps/ of/
/ / / integertyp:/ /(ival:/ integer/)/;/
/ / / realtyp:/ /(rval:/ real/)/;/
/ / / booleantyp:/ /(bval:/ boolean/)/;/
/ / / chartyp:/ /(cval:/ char/)/;/
/ / / symboltyp:/ /(sval:/ symbol/)/
/ / end/;/
/
/ sym1/ =/ record/
/ / notempty:/ boolean/;/
/ / firstch:/ char/;/
/ / tail:/ symbol/;/
/ / end/;/
/
/ varpairs/ =/ ↑vp/;/
/
/ vp/ =/ record/
/ / notempty:/ boolean/;/
/ / old:/ integer/;/
/ / new:/ integer/;/
/ / rest:/ varpairs/
/ / end/;/
/
))
;(def make-type-decs (typelist)
; (cond ((null typelist) ())
; (t (append (get (first typelist) 'type-dec)
; (make-type-decs (rest typelist))))))
;
;
;(def sift-types (var-type-list)
; (do ((l var-type-list (rest l))
; (typelist () (cons-if-new (rest (first l)) typelist)))
; ((null l) typelist)))
(def cons-if-new (x l)
(cond ((memq x l) l)
(t (cons x l))))
(def general-funs ()
'(function / occur(x/,/ y:/ term):/ boolean/;/
/ extern/;/
function/ genvar:/ integer/;/
/ extern/;/
procedure / replace(x/,/ t:/ term/;/ var/ tml:/ termlist)/;/
/ extern/;/
procedure/ subst(x/,/ t:/ term/;/ var/ t1/,/ t2:/ termlist)/;/
/ extern/;/
function/ eqsym(x/,/ y:/ symbol):/ boolean/;/
/ extern/;/
function/ eqconst(x/,/ y:/ constant):/ boolean/;/
/ extern/;/
function/ copysym(oldsym:/ symbol):/ symbol/;/
/ extern/;/
function/ copyterm(oldtm:/ term):/ term/;/
/ extern/;/
function/ copytermlist(tml:/ termlist):/ termlist/;/
/ extern/;/
function/ copyconst(oldconst:/ constant):/ constant/;/
/ extern/;/
function/ unify(var/ x/,y/,allx/,ally:termlist):/ boolean/;/
/ extern/;/
procedure/ Lookup(tm:/ term/;/ tbl:/ varpairs/;/ found:/ boolean)/;/
/ extern/;/
procedure/ Standapart(tml:/ termlist/;/ var/ donetbl:/ varpairs)/;/
/ extern/;/
))
(def make-external-decs (procnames)
(cond ((null procnames) (general-funs))
(t (append (mk-ext-dec (first procnames))
(make-external-decs (rest procnames))))))
(def mk-ext-dec (name)
((lambda (x)
(cond (x x)
(t (putprop name (list 'FUNCTION '/ name
(make-parameter-list (get name 'types)
(get name 'inpat))
': '/ 'boolean '/; '/
'/ 'EXTERN '/; '/
)
'extproc-head))))
(get name 'extproc-head)))
(def algol-ize (wff)
(cond ((atom wff) 'true)
((eq (first wff) '∧)
((lambda (arg1 arg2)
(cond ((eq arg1 'true) (cond ((eq arg2 'true) 'TRUE)
(t arg2)))
((eq arg2 'true) arg1)
(t (list arg1 'AND arg2))))
(algol-ize (second wff))
(algol-ize (third wff))))
((eq (first wff) '∨)
((lambda (arg1 arg2)
(cond ((eq arg1 'true) 'TRUE)
((eq arg2 'true) 'TRUE)
(t (list arg1 'OR arg2))))
(algol-ize (second wff))
(algol-ize (third wff))))
(t ((lambda (ans-code) ;o.w. it is a funapp, so generate
(setq pascode (append pascode ;pascal to represent the
(rest ans-code))) ;terms and build the
(list (first wff) ;new call
(insertcommas (first ans-code))))
(actualize (rest wff))))))
;(def mk-termlist (params) ;returns a list of stmnts building a termlist
; (cond ((null params) ()) ;"actuals" of the formal parameters. This is
; (t (append ;for use in the function body in order to call
; (list 'new '(p) '; '/ ;bktrkcond appropriately. actuals and
; 'p↑/.tl '/ ':= '/ 'actuals; '/ ;p are declared in the
; 'p↑/.hd '/ ':= '/ (first params) '; '/ ;body of the
; 'p↑/.sl '/ ':= '/ 'FALSE; '/ ;function as pointers
; 'actuals '/ ':= '/ 'p; '/ ;to termlists.
;)
; (mk-termlist (rest params))))))
(def make-try (trylist) ;gets called with the list of subgoals with
(cond ((null trylist) 'true) ;the "try" stripped off, and generates a
(t ((lambda (call) ;conjunction out of the subgoal calls
(cond ((null (rest trylist))
call)
(t (append call
'(AND)
(make-try (rest trylist))))))
(list (first (first trylist))
(rest (first trylist)))))))
;(def make-arglist (args inpat)
; (cond ((null args) '( '/) ) ) ;that's a list consisting of one right paren
; ((eq (first inpat) 0)
; (append (list ''/, (list 'quote (first args)))
; (make-arglist (rest args) (rest inpat))))
; (t (append
; (list ''/, ''val ''/( ''" (list 'quote (first args)) ''"
; ''/, ''s1 ''/) )
; (make-arglist (rest args) (rest inpat))))))
;body of a pascal function should look like:
; type decs
; var decs
; ext decs
; begin
; if algol-ized precond
; then begin
; build two copies of termlist with
; input actuals copied and
; output actuals newed terms of type var(gensymed?)
; build matchlist
; if unify-with first matchlist
; then build terms for unmentioned vars(?) and
; definitely build terms for unmentioned non-vars
; set failed to not conj of subgoals
; else set failed to true
; if failed
; then copy saved actuals (or mung the munged copy
; back the way it was)
; build the next matchlist
; if unify-with ...
; then...
; else set failed to true
; if failed
; ... for each alternative, but the last one doesn't
; have to make a new copy to work on
; formal output params get set to appropriate results
; name gets set to not failed
; end
; else name gets set to false
; end
;
(def stripdeep! (exp)
(cond ((atom exp) ((lambda (namelist)
(cond ((eq (first namelist) '!)
(implode (rest namelist)))
(t exp)))
(explode exp)))
(t (cons (stripdeep! (first exp))
(stripdeep! (rest exp))))))
(def insertcommas (arglist)
(cond ((null arglist) ())
(t (rest (inscom arglist)))))
(def inscom (arglist)
(cond ((null arglist) ())
(t (append (list '/, (first arglist))
(inscom (rest arglist))))))
(def make-body-of (name)
(prog (donelist local-vars pascode)
(setq local-vars '((actuals copyactuals matchlist) () () ()))
(setq donelist (strip! (get name 'params)))
(setq pascode
(append
'(BEGIN /
)
(prog (pascode)
(return
((lambda (stuff)
(append
pascode
'( if / )
stuff))
(list (algol-ize (stripdeep! (get name 'typedprecond))) '/
))))
'(then / begin /
)
(build-actuals (strip! (get name 'params)))
(do ((alts (reverse (stripdeep! (rest (get name 'body)))) (rest alts))
(ans () ((lambda (alt)
(setq donelist '(actuals copyactuals matchlist))
(append
'(copyactuals / := / copytermlist (actuals) /; /
new(donetbl)/;/
donetbl↑/.notempty/ :=/ false/;/
standapart (copyactuals/, donetbl)/;/
)
(mk-termlist 'matchlist (match-pt alt))
'(if / unify (copyactuals /, matchlist/, copyactuals/,
matchlist) /
then / begin /
)
((lambda (sbgls-code)
(append (rest sbgls-code)
(list 'failed '/ ':= '/ 'not '/
(make-try (first sbgls-code)) '/
'end '/
)))
(fix-subgoals (try-pt alt)))
'(else / failed / := / true /; /
)
ans))
(first alts))))
((null alts) ans))
(list 'flag '/ ':= '/ 'not '/ 'failed '/; '/
name '/ ':='/ 'flag'/;'/
'if '/ 'flag '/
'then '/ 'begin '/
)
(mk-assgns (strip! (get name 'params)))
(list 'end '/
'end '/
'else '/ name '/ ':= '/ 'false '/
'end '/;'/
)))
(return
(append
(make-local-decs local-vars)
'(/ donetbl:/ varpairs/;/
/ flag/,/ failed:/ boolean/;/
/
) pascode))))
(def mk-assgns (params)
(cond ((null params) ())
(t (append (list (first params) '/ ':= 'copyactuals↑/.first '/; '/
'copyactuals '/ ':='/ 'copyactuals↑/.rest '/; '/
) (mk-assgns (rest params))))))
;build-actuals generates the pascal code to build a termlist out of the actual
;parameters, the actuals are already of type term, so all it has to do is link
;them together into a termlist called actuals so they will be appropriate input
;to the unifier.
(def build-actuals (params)
(append
(list 'new '(actuals) '/; '/
'actuals↑/.notempty '/ ':= '/ 'false '/; '/
)
(do ((vars params (rest vars))
(ans () ((lambda (temp)
(addlocal-tml temp)
(append
(list 'new '/( temp '/) '/; '/
temp '↑'/.'notempty '/ ':= '/ 'true'/; '/
temp '↑ '/.'first '/ ':= '/ (first vars) '/;'/
temp '↑'/.'rest '/ ':= '/ 'actuals'/; '/
'actuals '/ ':= '/ temp '/; '/
)
ans))
(gensym))))
((null vars) ans))))
;mk-var creates a variable record, it stuffs a gensym in its integer slot, i think
;i'll dump the print name as unnecessary baggage *** no need for mk-var!!!
(def mk-termlist (name arglist) ;generates the pascal code to make a termlist,
(addlocal-tml name) ;pointed to by name, whose elements are made up
;of terms constructed from the elements of arglist.
;donelist is global (local to make-body) and is
;re-initialized whenever a new alternative is
;being translated. All variables created in this
;process (new'd) must be added to the list local-
;vars so that the appropriate declarations will be
;generated for them.
(append
(list 'new '/( name '/) '/; '/
name '↑ '/. 'notempty '/ ':='/ 'false '/; '/
)
(do ((args (reverse arglist) (rest args))
(ans () ((lambda (temp)
(addlocal-tml temp)
(append
(list 'new '/( temp '/) '/; '/
temp '↑ '/. 'notempty '/ ':='/ 'true '/;'/
)
(cond ((is-var (first args))
(cond ((memq (first args) donelist)
(list temp '↑'/.'first'/ ':='/
(first args)'/;'/
))
(t (mark-done (first args))
(append (mk-term (first args)
(first args))
(list temp '↑'/.'first '/ ':='/
(first args) '/; '/
)))))
(t ((lambda (tmname)
(append (mk-term tmname (first args))
(list temp'↑'/.'first '/ ':='/
tmname '/; '/
)))
(gensym))))
(list temp'↑'/.'rest '/ ':= '/ name '/; '/
name '/ ':='/ temp '/; '/
)
ans))
(gensym))))
((null args) ans))))
(def mk-term (name arg)
(prog (quotflag)
(addlocal-tm name)
(return
(append
(list 'new '/( name '/) '/; '/
)
(cond ((is-var arg)
(list name'↑'/.'ttyp '/ ':= '/ 'variable'/; '/
name '↑'/.'vr '/ ':= '/ 'genvar '/; '/
))
((is-constant arg)
(cond ((is-quoted arg) (setq quotflag t)
(setq arg (second arg))))
(cond ((atom arg)
(append (list name '↑'/.'ttyp '/ ':='/ 'constanttyp'/; '/
) ((lambda (con)
(append
(mk-const con arg)
(list name '↑'/.'cnst '/ ':='/ con'/;'/
)))
(gensym))))
(quotflag
(append (list name'↑'/.'ttyp '/ ':='/ 'funapp'/; '/
) (mk-sym 'cons (explode 'cons))
((lambda (tml)
(append
(mk-termlist tml (rest (cons-out arg)))
(list name'↑'/.'fname'/ ':='/ 'cons '/;'/
name'↑'/.'args '/ ':='/ tml'/; '/
)))
(gensym))))
(t (append
(list name'↑'/.'ttyp '/ ':='/ 'funapp'/; '/
) (mk-sym (first arg) (explode (first arg)))
((lambda (tml)
(mk-termlist tml (rest arg)))
(gensym))
(list name'↑'/.'fname'/ ':='/ (first arg)'/;'/
name'↑'/.'args '/ ':='/ tml'/; '/
)))))
(t (append
(list name'↑'/.'ttyp '/ ':='/ 'funapp'/; '/
) (mk-sym (first arg) (explode (first arg)))
((lambda (tml)
(mk-termlist tml (rest arg)))
(gensym))
(list name'↑'/.'fname'/ ':='/ (first arg)'/;'/
name'↑'/.'args '/ ':='/ tml'/; '/
))))))))
(def cons-out (list)
(cond ((null list) ())
(t (list 'cons (cond ((is-constant (first list)) (first list))
(t (list 'quote (first list))))
(cons-out (rest list))))))
(def mk-const (name atm)
(addlocal-cnst name)
(append (list 'new '/( name '/) '/;'/
)
(cond ((fixp atm) (list name'↑'/.'ctyp '/ ':= '/ 'integertyp'/; '/
name'↑'/.'ival '/ ':= '/ atm '/; '/
))
((floatp atm) (list name'↑'/.'ctyp '/ ':='/ 'realtyp'/; '/
name'↑'/.'rval '/ ':='/ atm '/; '/
))
((eq atm t) (list name'↑'/.'ctyp '/ ':='/ 'booleantyp'/; '/
name'↑'/.'bval '/ ':= '/ 'true'/; '/
))
((eq atm false) (list name'↑'/.'ctyp '/ ':='/ 'booleantyp'/; '/
name'↑'/.'bval '/ ':= '/ 'false'/; '/
))
(t (append (list name'↑'/.'ctyp '/ ':='/ 'symboltyp'/; '/
) (mk-sym arg (explode arg))
(list name'↑'/.'sval '/ ':= '/ arg'/; '/
))))))
(def is-quoted (x) (cond ((atom x) nil)
(t (eq (first x) 'quote))))
(def mk-sym (name charlist)
(cond
((memq name donelist) ())
(t
(addlocal-sym name)
(append (list 'new '/( name '/)'/;'/
name '↑ '/. 'notempty '/ ':='/ 'false'/;'/
)
(do ((chars (reverse charlist) (rest chars))
(ans () ((lambda (temp)
(addlocal-sym temp)
(append
(list 'new '/( temp '/)'/; '/
temp '↑'/.'notempty '/ ':='/ 'true'/;'/
temp '↑'/.'firstch '/ ':='/ (first chars)'/;'/
temp '↑'/.'tail '/ ':='/ name'/; '/
name '/ ':='/ temp '/;'/
)
ans))
(gensym))))
((null chars) ans))))))
(def fix-subgoals (sbglist) ;makes a list of subgoals whose arglists are lists
(cond ;of terms for which the pascal code has been
((null sbglist)'(())) ;generated. its value is the new sbglist cons onto
(t ((lambda (first-ans rest-ans) ;the list of pascal stuff
(cons
(cons (cons (first (first sbglist)) ;i.e., subgoal name
(insertcommas
(first first-ans))) ;i.e., new arglist
(first rest-ans)) ;the other subgoals
(append (rest first-ans) ;p-code for this subgoal
(rest rest-ans)))) ;p-code for the rest of the subgoals
(actualize (rest (first sbglist))) ;generates stuff for one arglist
(fix-subgoals (rest sbglist))))))
(def actualize (arglist) ;turns an arglist in intermediate form, into a list
(cond ;of terms- the value is the new arglist cons'd onto
((null arglist)'(())) ;the list of p-code
(t ((lambda (arg-ans rest-ans)
(cons (cons (first arg-ans)
(first rest-ans))
(append (rest arg-ans)
(rest rest-ans))))
(arg-to-term (first arglist))
(actualize (rest arglist))))))
(def arg-to-term (arg)
(cond
((is-var arg)
(cond ((memq arg donelist) (list arg))
(t (cons arg (mk-term arg arg)))))
(t ((lambda (name)
(cons name
(mk-term name arg)))
(gensym)))))
;local-vars and donelist are global to several of the above functions. They are
;the means by which information about which terms have been generated and
;must be declared are transmitted about. Local-vars is a list of 4 lists of
;variables that must be declared as termlists, terms, constants, and symbols,
;respectively. Every time a new variable is created it is added to this list
;in the appropriate type sublist. Whenever a variable (pointer) is created
;that may appear again, it is added to donelist so that multiple versions
;need not be generated.
(def mark-done (name) (setq donelist (cons-if-new name donelist)))
(def addlocal-tml (name)
(setq local-vars (cons (cons-if-new name (first local-vars))
(rest local-vars))))
(def addlocal-tm (name)
(setq local-vars (cons (first local-vars)
(cons (cons-if-new name (second local-vars))
(rest (rest local-vars))))))
(def addlocal-cnst (name)
(setq local-vars (cons (first local-vars)
(cons (second local-vars)
(cons (cons-if-new name (third local-vars))
(rest (rest (rest local-vars))))))))
(def addlocal-sym (name)
(setq local-vars (cons (first local-vars)
(cons (second local-vars)
(cons (third local-vars)
(cons (cons-if-new name (fourth local-vars))
()))))))
(*pascal programs*)
(*$E+*)
program junk,unify,subst,replace,copytermlist,copyterm,copyconst,copysym;
(*pascal can't handle things the way it should so we have to invent strange
names that are all referring to the same thing, in particular, the type
of the object at hand. Thus,
alltyps, an indication of the possible atomic types, is actually made
up of convoluted versions of the type names.
this idiocy is carried on throughout, which is why you'll see several
different names that all look similar but had to be different for pascal. *)
TYPE
(* alltyps are the types of atomic constants *)
alltyps = (integertyp, realtyp, booleantyp, chartyp, symboltyp);
termtyps = (variable, constanttyp, funapp);
term = ↑t1;
termlist = ↑tl1;
constant = ↑c1;
symbol = ↑sym1;
t1 = record
case ttyp:termtyps of
variable: (vr: integer);
constanttyp: (cnst: constant);
funapp: (fname: symbol;
args: termlist)
end;
tl1 = record
notempty: boolean;
first: term;
rest: termlist
end;
(*changed again: a variable is just an integer, serves fine for
comparison and we never print them out anyway*)
(* variable = symbol; *) (*vars have names and are free, when they
get bound they are replaced by other terms*)
(* variable = ↑v1;
v1 = record
bound: boolean;
pname: symbol;
case vtyp:alltyps of
integer: (ival: integer);
real: (rval: real);
boolean: (bval: boolean);
char: (cval: char);
term: (tval: term)
end; *)
c1 = record
case ctyp:alltyps of
integertyp: (ival: integer);
realtyp: (rval: real);
booleantyp: (bval: boolean);
chartyp: (cval: char);
symboltyp: (sval: symbol)
end;
sym1 = record
notempty: boolean;
firstch: char;
tail: symbol
end;
varpairs = ↑vp;
vp = record
notempty: boolean;
old: integer;
new: integer;
rest: varpairs
end;
(* singlesub = ↑ss1;
ss1 = record
vr: variable;
tm: term
end;
sub = ↑s1;
s1 = record
failed: boolean;
isempty: boolean;
first: singlesub;
rest: sub
end;
*)
(*Var x1, y1: termlist;
x2, y2: term;
s2: sub;
Begin
*initialize: s gets the empty substitution*
new(s);
s↑.isempty := true;
s↑.failed := false;
x1 := x; (*these are here because they were in fwh's version*
y1 := y;
while x1↑.notempty and y1↑.notempty and not(s↑.failed) do
begin
termsubst( x1↑.first, s, x2);
termsubst( y1↑.first, s, y2);
if x2↑.ttyp = variable
then begin
if y2↑.ttyp = variable
then begin
if not( eqsym(x2↑.vr↑.pname, y2↑.vr↑.pname) )
(*pascal can't handle this comparison itself, records,you know*
then composesub( s, pair(x2↑.vr, y2));
(*if they are the same variable then nothing need be done*
end
else if occur(x2, y2)
then s↑.failed := true
else composesub( s, pair(x2↑.vr, y2))
end
else if y2↑.ttyp = variable
then begin
if occur(y2, x2)
then s↑.failed := true
else composesub(s, pair(y2↑.vr, x2))
end
else if x2↑.ttyp = constant
then begin
if y2↑.ttyp = constant
then begin
if not( eqconst(x2↑.cnst, y2↑.cnst) )
then s↑.failed := true;
(*if they are = nothing need be done*
end
else if x2↑.cnst↑.ctyp = term
then begin
matchconst(x2↑.const↑.tval, y2, s2);
if s2↑.failed
then s↑.failed := true
else composesub (s, s2)
end
else s↑.failed := true;
(*any other kind of constant could only
match with a variable*
end
else (*x2 is a funapp (thus of type term) and y2 is not a variable
if y2↑.ttyp = constant
then begin
if y2↑.cnst↑.ctyp = term
then begin
matchconst(y2↑.cnst↑.tval, x2, s2);
if s2↑.failed
then s↑.failed := true
else composesub(s, s2)
end
else s↑.failed := true
end
else (*x2 and y2 are both funapp terms*
if eqsym(x2↑.fname, y2↑.fname)
then begin
unify(x2↑.args, y2↑.args, s2);
if s2↑.failed
then s↑.failed := true
else composesub(s, s2)
end
else s↑.failed :=true;
x1 := x1↑.rest;
y1 := y1↑.rest
end; (*of while*
if x1↑.notempty or y1↑.notempty then s↑.failed := true
End; (*of unify*
*)
(*unify side effects its args all over the place, the originals are copied before
the call is made*)
(*
Procedure unify(var x, y: termlist; failed:boolean);
Var x1, y1: termlist;
x2, y2: term;
subfailed: boolean;
Begin
(*initialize*
failed := false;
x1 := x;
y1 := y;
while x1↑.notempty and y1↑.notempty and not(failed) do
begin
x2 := x1↑.first;
y2 := y1↑.first;
if x2↑.ttyp = variable
then begin
if y2↑.ttyp = variable
then x2↑.vr↑.pname := y2↑.vr↑.pname
(* if they're already the same, the assignment is unnecessary
but cheaper than testing the equality and won't hurt anything*
else if occur(x2, y2)
then failed := true
else subst(x2↑.vr, y2, x, y)
end
else if y2↑.ttyp = variable
then begin
if occur(y2, x2)
then failed := true
else subst(y2↑.vr, x2, x, y)
end
else if x2↑.ttyp = constant
then begin
if y2↑.ttyp = constant
then begin
if not( eqconst(x2↑.cnst, y2↑.cnst) )
then failed := true;
(*if they are = nothing need be done*
end
else if x2↑.cnst↑.ctyp = term
then begin
matchconst(x2↑.const↑.tval, y2, x, y, subfailed);
if subfailed
then failed := true
end
else failed := true;
(*any other kind of constant could only
match with a variable*
end
else (*x2 is a funapp (thus of type term) and y2 is not a variable*
if y2↑.ttyp = constant
then begin
if y2↑.cnst↑.ctyp = term
then begin
matchconst(y2↑.cnst↑.tval, x2, x, y, subfailed);
if subfailed
then failed := true
end
else failed := true
end
else (*x2 and y2 are both funapp terms*
if eqsym(x2↑.fname, y2↑.fname)
then begin
unify(x2↑.args, y2↑.args, subfailed);
if subfailed
then failed := true
end
else failed :=true;
x1 := x1↑.rest;
y1 := y1↑.rest
end; (*of while*
if x1↑.notempty or y1↑.notempty then failed := true
End; (*of unify*
*)
(* the true glory of the new type defs shows up here... no matchconst is necessary!
Procedure Matchconst(x, y, allx, ally: term; var failed: boolean);
Var x1, y1: termlist;
subfailed: boolean;
Begin
failed := false;
if y↑.ttyp = variable
then subst(y↑.vr, x, allx, ally)
else if y↑.ttyp = constant
then begin
if not(eqconst(x, y↑.cnst))
then failed := true
end (*if they're the same then nothing need be done*
else if x↑.ttyp = funapp
then begin
if eqsym(y↑.fname, x↑.fname)
then begin
x1 := x↑.args;
y1 := y↑.args;
while x1↑.notempty and y1↑.notempty and not(failed)
do begin
Matchconst(x1↑.first, y1↑.first, allx, ally, subfailed);
if subfailed
then failed := true
end
end
else failed := true
end
else failed := true
End; (*matchconst*
*)
Function Genvar:Integer;
begin
genvar:= realtime
end;(*genvar*)
Function occur(x,y:term):boolean;
Var ptr: termlist;
flag: boolean;
begin
if y↑.ttyp = variable
then begin
if y↑.vr = x↑.vr
then occur := true
else occur := false
end
else if y↑.ttyp = constanttyp
then occur := false
else begin
ptr := y↑.args;
flag := false;
while ptr↑.notempty and (flag = false)
do begin
flag := occur(x, ptr↑.first);
ptr := ptr↑.rest
end;
occur := flag
end
end;(*occur*)
Procedure Replace(x, t: term; var tml: termlist);
Var tl1:termlist;
t1:term;
Begin
tl1:= tml;
while tl1↑.notempty do
begin
t1 := tl1↑.first;
if not(t1↑.ttyp = constanttyp)
then begin
if t1↑.ttyp = variable
then begin
if x↑.vr = t1↑.vr
then (*t1 gets t, but i dont think an assignment will work;
try it anyway, think about it later*)
tl1↑.first := t (*need to mung record, not just ptr t1*)
(*else, no change needed*)
end
else (*it's a funapp*)
replace(x, t, tl1↑.first↑.args)
end;
(*if its a constant no changes need be made*)
tl1 := tml↑.rest
end (*of while*)
End; (*replace*)
Procedure Subst(x, t:term; var t1, t2:termlist);
Begin
replace(x, t, t1);
replace(x, t, t2)
End;
Function Eqsym(x,y:symbol):boolean;
Begin
while x↑.notempty and y↑.notempty and (x↑.firstch = y↑.firstch) do
begin
x:=x↑.tail;
y:=y↑.tail
end;
if x↑.notempty or y↑.notempty
then eqsym:= false
else eqsym:= true
End;
Function eqconst(x,y:constant):boolean;
Begin
if x↑.ctyp = y↑.ctyp
then case x↑.ctyp of
integertyp: eqconst:= x↑.ival = y↑.ival;
realtyp: eqconst:= x↑.rval = y↑.rval;
booleantyp: eqconst:= x↑.bval = y↑.bval;
chartyp: eqconst:= x↑.cval = y↑.cval;
symboltyp: eqconst:= eqsym(x↑.sval, y↑.sval)
end
else eqconst:= false
End;
Function Copysym(oldsym:symbol):symbol;
Var newsym, lastnode, newnode:symbol;
Begin
new(newsym);
lastnode := newsym;
while oldsym↑.notempty do
begin
lastnode↑.notempty := true;
lastnode↑.firstch := oldsym↑.firstch;
new(newnode);
lastnode↑.tail := newnode;
lastnode := newnode;
oldsym := oldsym↑.tail
end;
lastnode↑.notempty := false;
copysym := newsym
End; (*Copysym*)
Function Copyterm(oldtm:term):Term;
forward;
Function Copytermlist(tml:termlist):Termlist;
Var newnode, lastnode, tmlnew:termlist;
Begin
new(tmlnew);
lastnode := tmlnew;
while tml↑.notempty do
begin
lastnode↑.notempty := true;
lastnode↑.first := copyterm(tml↑.first);
new(newnode);
lastnode↑.rest := newnode;
lastnode := newnode;
tml := tml↑.rest;
end;
lastnode↑.notempty := false;
copytermlist := tmlnew
End; (*copytermlist*)
Function Copyconst(oldconst:constant):Constant;
Var newconst:constant;
Begin
new(newconst);
newconst↑.ctyp := oldconst↑.ctyp;
case newconst↑.ctyp of
integertyp: newconst↑.ival := oldconst↑.ival;
realtyp: newconst↑.rval := oldconst↑.rval;
booleantyp: newconst↑.bval := oldconst↑.bval;
chartyp: newconst↑.cval := oldconst↑.cval;
symboltyp: newconst↑.sval := copysym(oldconst↑.sval)
end; (*of case stmt*)
copyconst := newconst
End; (*Copyconst*)
Function Copyterm;
Var newtm:term;
Begin
new(newtm);
newtm↑.ttyp := oldtm↑.ttyp;
case newtm↑.ttyp of
variable: newtm↑.vr := oldtm↑.vr; (*it's just an integer*)
constanttyp: newtm↑.cnst := copyconst(oldtm↑.cnst);
funapp: begin
newtm↑.fname := copysym(oldtm↑.fname);
newtm↑.args := copytermlist(oldtm↑.args)
end
end; (*of case stmt*)
copyterm := newtm
End; (*Copyterm*)
(* a copy is made once, before the unifier is called, so that
a unification can be undone if it is not successful or it leads to an unsuccessful
subgoal. the allx and ally args are necessary to ensure that any replacements
resulting from recursive calls get made throughout the entire termlists you started
with
the first call on unify will repeat the arglists being unified- dumb, but it
makes it possible to accomplish the substitutions by replacement as we go instead
of building a substitution and making new copies of everything every time we do
a substitution. *)
Function unify(var x, y, allx, ally: termlist): boolean;
Var x1, y1: termlist;
x2, y2: term;
dummy, failed: boolean;
Begin
(*initialize*)
failed := false;
x1 := x;
y1 := y;
while x1↑.notempty and y1↑.notempty and not(failed) do
begin
x2 := x1↑.first;
y2 := y1↑.first;
if x2↑.ttyp = variable
then begin
if y2↑.ttyp = variable
then x2↑.vr := y2↑.vr
(* if they're already the same, the assignment is unnecessary
but cheaper than testing the equality and won't hurt anything*)
else if occur(x2, y2)
then failed := true
else subst(x2, y2, x, y)
end
else if y2↑.ttyp = variable
then begin
if occur(y2, x2)
then failed := true
else subst(y2, x2, x, y)
end
else if x2↑.ttyp = constanttyp
then begin
if y2↑.ttyp = constanttyp
then begin
if not( eqconst(x2↑.cnst, y2↑.cnst) )
then failed := true;
(*if they are = nothing need be done*)
end
else failed := true
end
else (*x2 is a funapp and y2 is not a variable*)
if y2↑.ttyp = constanttyp
then failed := true
else (*x2 and y2 are both funapp terms*)
if eqsym(x2↑.fname, y2↑.fname)
then begin
dummy :=
unify(x2↑.args, y2↑.args,
allx, ally);
if not dummy
then failed := true
end
else failed :=true;
x1 := x1↑.rest;
y1 := y1↑.rest
end; (*of while*)
if x1↑.notempty or y1↑.notempty then failed := true;
unify := not failed
End; (*of unify*)
Function Lessthan(x, y:term; var z:term):boolean;
var con: constant;
begin
z↑.ttyp := constanttyp;
new(con);
z↑.cnst := con;
con↑.ctyp := booleantyp;
if x↑.cnst↑.ival < y↑.cnst↑.ival
then z↑.cnst↑.bval := true
else z↑.cnst↑.bval := false;
Lessthan := true
end;
Function greaterequal(x, y:term; var z: term): boolean;
var con: constant;
begin
z↑.ttyp := constanttyp;
new(con);
con↑.ctyp := booleantyp;
z↑.cnst := con;
if x↑.cnst↑.ival >= y↑.cnst↑.ival
then z↑.cnst↑.bval := true
else z↑.cnst↑.bval := false;
Greaterequal := true
end;
function times(x, y:term; var z:term): boolean;
var con:constant;
begin
z↑.ttyp := constanttyp;
new(con);
con↑.ctyp := integertyp;
z↑.cnst := con;
con↑.ival := x↑.cnst↑.ival * y↑.cnst↑.ival;
times := true
end;
function sub1(x: term; var y:term):boolean;
var con:constant;
begin
y↑.ttyp := constanttyp;
new(con);
con↑.ctyp := integertyp;
y↑.cnst := con;
con↑.ival := x↑.cnst↑.ival - 1;
sub1 := true
end;
Procedure Lookup(tm:term; tbl: varpairs; found: boolean);
var ptr: varpairs;
begin
found := false;
ptr := tbl;
while ptr↑.notempty and not found
do begin
if ptr↑.old = tm↑.vr
then begin
tm↑.vr := ptr↑.new;
found := true
end;
ptr := ptr↑.rest
end
end; (*lookup*)
Procedure Standapart(tml: termlist; var donetbl: varpairs);
var ptr: termlist;
done: varpairs;
found: boolean;
begin
ptr:= tml;
while ptr↑.notempty
do begin
if ptr↑.first↑.ttyp = variable
then begin
lookup(ptr↑.first, donetbl, found);
if not found
then begin
new(done);
done↑.notempty := true;
done↑.old := ptr↑.first↑.vr;
done↑.new := genvar;
ptr↑.first↑.vr := done↑.new;
done↑.rest := donetbl;
donetbl := done
end
end
else if ptr↑.first↑.ttyp = funapp
then standapart(ptr↑.first↑.args, donetbl);
ptr := ptr↑.rest
end
end; (*standapart*)
begin (*junk*)
end.